『Homotopy Type Theory Univalent Foundations of Mathematics』

ホモトピー型理論(Homotopy Type Theory; HoTT)の経典？のようなとてもまとまった本

Introduction

P1～P14

型、論理、集合、ホモトピーの対応はHoTTの本に書いてあった。翻訳したものは下記。

$ \begin{array}{c|c|c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) & 集合(\mathrm{Sets}) & ホモトピー \\ \hline A & 命題 & 集合 & 空間 \\ a: A & 証明 & 元 & 点 \\ B(x) & 述語 & 集合の族 & ファイブレーション \\ b(x) : B(x) & \mathrm{条件付き証明} & 元の族 & \mathrm{切断} \\ \bm{0, 1} & \bot , \top & \varnothing , \{ \varnothing \} & \varnothing, * \\ A + B & A \lor B & \mathrm{非交和} & 余積 \\ A \times B & A \land B & 組の集合 & 積の空間 \\ A \to B & A \implies B & 関数の集合 & 関数空間 \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) & \mathrm{直和} & \mathrm{全空間 } \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) & 積 & 切断の空間 \\ \mathrm{Id}_A & 等号\ = & \lbrace (x, x) | x \in A \rbrace & 道空間A^I \end{array}

ref: Table 1: Comparing points of view on type-thoretic operations (P11)

table:訳

英語 日本語

element 元

point 点

family of sets 集合の族

section 断面 or 切断

conditional proof 条件付き証明

family of sets 集合の族

set of pairs 組の集合

product space 積の空間

set of function 関数の集合

function space 関数空間

total space 全空間、全体空間？

product 直積

space of section 切断の空間 or セクションの空間？

equality 等号

path space 道空間

object 対象

rule 規則

judgements 判断

deductive system 演繹系

assumption 仮定

pointwise 点別の

moment in time その瞬間で

analogously 類似の方法で

familiar おなじみの

homotopy colimit ホモトピー余極限

suspension 懸垂

localization 局所化

spectrification スペクトロフィケーション？

nth Postnikov section n番目ポストニコフ断面

(−1)-truncated logic

intuitionistic 直観主義

endpoint 端点

LEM Law of Excluded middle(排中律)

AC Axiom of Choice(選択公理)

cannonical mapping 自然な写像？、

property 性質

Freudenthal suspension theorem フロイデンタールの懸垂定理

universe 宇宙

identity

equivalent types

small type

contractible 可縮

transfinite 超限、有限を超える

judgmentally equal 判断として等しい

(propositionally) equal 命題として等しい

table:訳2

英語 訳

definitionally 定義上

prescribing 処方する

Unsurprisingly 当然のことながら

Constructivity 構成性

striking 顕著な

stratified 層化？

presume 〔～を〕推定する、推測する、仮定する

inchoate 不完全な、未完成の

undergraduate 学部生

Open problems 未解決の問題

$ \mathrm{Id}_{\mathcal{U}} (A, B) = \mathrm{Equiv}(A, B)

Univalence Axiom

$ (A = B) \simeq (A \simeq B)

形式的に書くと下記になる

$ \mathrm{Iso}(A, B) :\equiv \sum_{(f:A \to B)} \sum_{(g:B \to A)}\left \lparen \lparen \prod_{(x:A)}g(f(x)) = x \rparen \times \lparen \prod_{(y:B)} f(g(y) = y)\rparen \right\rparen

型コンストラクタΣ,Π,×をそれぞれ「存在する」,「すべて存在する」,「and」と言い換えられる

Table1より

$ \begin{array}{cc} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) \\ \prod_{x:A}B(x) & \forall_{x:A} B(x) \\ A \times B & A \land B \end{array}

stratified (…に)層を形成させる、 (…を)層状にする

Kol32, TvD88a, TvD88b

Kol32: Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35:58–65, 1932. (Cited on page 9.)

TvD88a: Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. I, volume 121 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. An introduction. (Cited on pages 9 and 127.)

TvD88b: Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. An introduction. (Cited on pages 9 and 127.)

n-truncated logic

TV02, Rez05, Lur09

TV02: Bertrand To ̈ en and Gabriele Vezzosi. Homotopical algebraic geometry I: Topos theory, 2002. arXiv:math/0207028. (Cited on page 10.)

Lur09: Jacob Lurie. Higher topos theory. Number 170 in Annals of Mathematics Studies. Princeton University Press, 2009. arXiv:math.CT/0608040. (Cited on pages 10, 146, 252, and 298.)

KLV12, LS17

KLV12: Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations, 2012. arXiv:1211.2851. (Cited on pages 11, 103, 175, and 441.)

LS17: Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. arXiv:1705.07088, 2017. (Cited on pages 11, 175, 218, and 441.)

$ \pi_1(\mathbb{S^1}) = \mathbb{Z}

Chapter 1 Type Thoery

Chapter 2 Homotopy type theory

Chapter 8 Homotopy theory

Chapter 9 Category theory

メモ

確認用

Q. HoTT

Q. dependent type theory

関連